-- import unificator, reductor

-- one, two, 
module LambdaCombinatorsSample where
import Data.List
import Text.Show.Functions
import Language.Haskell.Exts.Parser

-- Example combinators
data Expr = Var String | App Expr Expr | Lam String Expr 

instance Show Expr where
    show (Var s)       = s
    show (App e1 e2)  = "("++(show e1)++" "++(show e2)++")"
    show (Lam s e)    = "\\\\"++s++"."++(show e)

[z,s,m,n] = map (Var . (:[])) "zsmn"
app2 f x y = App (App f x) y
zero  = Lam "s" $ Lam "z" z
one   = Lam "s" $ Lam "z" $ App s z
two   = Lam "s" $ Lam "z" $ App s $ App s z
three = Lam "s" $ Lam "z" $ App s $ App s $ App s z
plus  = Lam "m" $ Lam "n" $ Lam "s" $ Lam "z" $ app2 m s (app2 n s z)

-- Samples  (look below for parseExp)
i3     = parseExp "\\x.x"
k3     = parseExp "\\x.\\y.x"
s3     = parseExp "\\x.\\y.\\z.((x z) (y z))"
ea3    = parseExp "(x (\\y.(y x) \\z.z))"
omega3 = parseExp "(\\x.(x x) \\x.(x x))"
skk3   = App (App s k) k

-- Church Booleans
true  = parseExp "\\t.\\f.t"
false = parseExp "\\t.\\f.f"
test  = parseExp "\\a.\\b.\\c. ((a b) a)"
cbAnd = parseExp "\\a.\\b. ((a b) \\t.\\f.f)"

-- Church numerals
churchNum :: Int -> Expr
churchNum n = Lam "s" (Lam "z" (rec n))
    where
      rec 0 = Var "z"
      rec n = App (Var "s") (rec (n-1))

--add           = parseExp "\\m.\\n.\\s.\\z.((m s) ((n s) z))"
--mul           = parseExp "\\m.\\n.\\s.\\z.((m (n s)) z)"
--twoPlusThree  = LambdaCombinatorsSample.App (LambdaCombinatorsSample.App add (churchNum 2)) (churchNum 3)
--threeTimesTwo = App (App mul (churchNum 3)) (churchNum 2)
--twoTimesThree = App (App mul (churchNum 2)) (churchNum 3)

--suc
--prd
--pair


-- I combinators
id = (Lam "x" $ Var "x")

-- K combinators(constant combinator (const in Haskell))
k = (Lam "x" $ Lam "y" $ Var "x")
k2 = (Lam "x" $ Lam "y" $ Var "y")                       


-- example
t1 = (App (Lam "x" $ Lam "y" $ Var "x") (Lam "z" $ Var "z"))
t2 = (App (Lam "x" $ Var "x") (Lam "z" $ Var "z"))
t3 = (App (Lam "x" $ Var "xx") (Lam "z" $ Var "zz"))
t4 = (Lam "x" $ Var "x")

-- K combin
t5 = (Lam "x" (Lam "y" (Var "x")))

